\begin{tabbing}
$\forall$${\it es}$:ES, $e$:E, $l$:IdLnk, ${\it tg}$:Id, $T$:Type, $v$:$T$.
\\[0ex]\{$m$:Msg$\mid$ source(mlnk($m$)) $=$ source($l$) $\in$ Id \}
\\[0ex]$\subseteq\rho$ Msg($\lambda$${\it l'}$,${\it tg'}$. if ${\it l'}$ = $l$ $\wedge_{2}$ ${\it tg'}$ = ${\it tg}$$\rightarrow$ $T$ else Top fi)
\\[0ex]$\Rightarrow$ sends($l$;$e$) $=$ [msg($l$;${\it tg}$;$v$)] $\in$ Msg($\lambda$${\it l'}$,${\it tg'}$. if ${\it l'}$ = $l$ $\wedge_{2}$ ${\it tg'}$ = ${\it tg}$$\rightarrow$ $T$ else Top fi) List
\\[0ex]$\Rightarrow$ (\=$\exists$${\it e'}$:E.\+
\\[0ex]kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd \& val(${\it e'}$) $=$ $v$ \& sender(${\it e'}$) $=$ $e$
\\[0ex]\& ($\forall$${\it e''}$:E. kind(${\it e''}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd $\Rightarrow$ sender(${\it e''}$) $=$ $e$ $\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$))
\-
\end{tabbing}